es:ES, T:Type, X:MaInterface(T). ma-interface-consistent2(es;X)   

latex

Definitions	ES, t  T, Type, x:A. B(x), MaInterface(T), Top, IdDeq, P  Q, ma-interface-ds(I;i), Id, x.A(x), x. t(x), f(x)?z, vartype(i;x), x:AB(x), loc(e), s = t, E, {x:A| B(x)} , ma-interface-valtype(I;i;k), valtype(e), kind(e), , Knd, e@i. P(e), x:A  B(x), P & Q, type List, b, S  T, ma-interface-dom(I;i), (x  l), hasloc(k;i), ma-interface-locs(I), ma-interface-consistent2(es;I)
Lemmas	ma-interface-locs wf, Knd wf, assert wf, hasloc wf, l member wf, ma-interface-dom wf, alle-at wf, es-kind wf, es-valtype wf, ma-interface-valtype wf, es-E wf, es-loc wf, subtype rel wf, es-vartype wf, fpf-cap wf, Id wf, ma-interface-ds wf, id-deq wf, top wf, ma-interface wf, event system wf